;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "Imerge-sort.lisp")

(interface Imerge-sort-private
  (sig is-permutation (xs ys))
  (sig in-increasing-order (xs)))
  
(module Mmerge-sort-private

  (defun split (n xs)
    (if (and (posp n) (consp xs))
        (let* ((x (car xs))
               (s (split (- n 1) (cdr xs)))
               (fr (car s))
               (bk (cadr s)))
          (list (cons x fr) bk))
        (list nil xs)))
  
  (defun merge (xs ys)         ; assume xs and ys are sorted
    (let ((x (car xs))
          (sx (cdr xs))
          (y (car ys))
          (sy (cdr ys)))
      (cond
        ((endp xs) ys)
        ((endp ys) xs)
        ((< (cadr x) (cadr y))
         (cons x (merge sx ys)))
        (t
         (cons y (merge xs sy))))))
  
  (defun merge-sort (xs)
    (if (consp (cdr xs))
        (let ((halves (split (floor (len xs) 2) xs)))
          (merge (merge-sort (car halves))
                 (merge-sort (cadr halves))))
        xs))
  
  (defun delete-element (x xs)
    (if (endp xs)
        xs
        (if (equal x (car xs))
            (cdr xs)
            (cons (car xs) (delete-element x (cdr xs))))))
  
  (defun is-permutation (xs ys)
    (or (and (endp xs) (endp ys))
        (and (consp xs)
             (member-equal (car xs) ys)
             (is-permutation (cdr xs) (delete-element (car xs) ys)))))
  
  (defun in-increasing-order (xs)
    (if (endp (cdr xs))
        t
        (and (<= (car xs) (cadr xs)) (in-increasing-order (cdr xs)))))

  
  (export Imerge-sort-private)
  (export Imerge-sort))

(link Mmerge-sort
      (import)
      (export Imerge-sort)   ;       specifies names visible
      (Mmerge-sort-private)) ;       in Mmerge-sort
